\begin{tabbing}
single{-}thread{-}generator\{i:l\}(${\it es}$;$P$;$R$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:E. Dec($P$($e$)))\+
\\[0ex]\& ($\forall$$e$, ${\it e'}$:E. Dec($R$(${\it e'}$,$e$)))
\\[0ex]\& $R$ =$>$ $\lambda$$x$,$y$. ($x$ $<$ $y$)
\\[0ex]\& ($\forall$$e$, ${\it e'}$:E. ($P$($e$) \& $R$(${\it e'}$,$e$)) $\Rightarrow$ $P$(${\it e'}$))
\\[0ex]\& (\=$\forall$$m$, ${\it m'}$:E.\+
\\[0ex]$P$($m$)
\\[0ex]$\Rightarrow$ $P$(${\it m'}$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($e$ $R$ $m$) $\Rightarrow$ ($\neg$$P$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($e$ $R$ ${\it m'}$) $\Rightarrow$ ($\neg$$P$($e$)))
\\[0ex]$\Rightarrow$ ($m$ = ${\it m'}$))
\-\\[0ex]\& ($\forall$$a$, $b$, $e$:E. ($R$($e$,$a$) \& $R$($e$,$b$)) $\Rightarrow$ ($P$($e$) \& $P$($a$) \& $P$($b$)) $\Rightarrow$ ($a$ = $b$))
\-
\end{tabbing}